Runtime Complexity (innermost) proof of /tmp/tmpQxWNgn/direct.xml

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CdtProblem

    ↳3 CdtInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳4 CdtProblem

    ↳5 CdtInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtInstantiationProof (BOTH BOUNDS(ID, ID), 5 ms)

    ↳8 CdtProblem

    ↳9 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 58 ms)

    ↳10 CdtProblem

    ↳11 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳12 CdtProblem

    ↳13 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 69 ms)

    ↳14 CdtProblem

    ↳15 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 67 ms)

    ↳16 CdtProblem

    ↳17 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 81 ms)

    ↳18 CdtProblem

    ↳19 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 357 ms)

    ↳20 CdtProblem

    ↳21 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 505 ms)

    ↳22 CdtProblem

↳23 CpxTrsMatchBoundsTAProof (⇔, 454 ms)

↳24 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

h(x, c(y, z)) → h(c(s(y), x), z)
h(c(s(x), c(s(0), y)), z) → h(y, c(s(0), c(x, z)))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(z0, c(z1, z2)) → c1(H(c(s(z1), z0), z2))
H(c(s(z0), c(s(0), z1)), z2) → c2(H(z1, c(s(0), c(z0, z2))))

S tuples:

H(z0, c(z1, z2)) → c1(H(c(s(z1), z0), z2))
H(c(s(z0), c(s(0), z1)), z2) → c2(H(z1, c(s(0), c(z0, z2))))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c1, c2

(3) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace H(z0, c(z1, z2)) → c1(H(c(s(z1), z0), z2)) by

H(c(s(x1), x0), c(z1, z2)) → c1(H(c(s(z1), c(s(x1), x0)), z2))
H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(c(s(z0), c(s(0), z1)), z2) → c2(H(z1, c(s(0), c(z0, z2))))
H(c(s(x1), x0), c(z1, z2)) → c1(H(c(s(z1), c(s(x1), x0)), z2))
H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))

S tuples:

H(c(s(z0), c(s(0), z1)), z2) → c2(H(z1, c(s(0), c(z0, z2))))
H(c(s(x1), x0), c(z1, z2)) → c1(H(c(s(z1), c(s(x1), x0)), z2))
H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c2, c1

(5) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace H(c(s(x1), x0), c(z1, z2)) → c1(H(c(s(z1), c(s(x1), x0)), z2)) by

H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(x2), c(s(x0), x1)), c(z2, z3)) → c1(H(c(s(z2), c(s(x2), c(s(x0), x1))), z3))
H(c(s(s(0)), x0), c(x1, x2)) → c1(H(c(s(x1), c(s(s(0)), x0)), x2))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(c(s(z0), c(s(0), z1)), z2) → c2(H(z1, c(s(0), c(z0, z2))))
H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))
H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(x2), c(s(x0), x1)), c(z2, z3)) → c1(H(c(s(z2), c(s(x2), c(s(x0), x1))), z3))
H(c(s(s(0)), x0), c(x1, x2)) → c1(H(c(s(x1), c(s(s(0)), x0)), x2))

S tuples:

H(c(s(z0), c(s(0), z1)), z2) → c2(H(z1, c(s(0), c(z0, z2))))
H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))
H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(x2), c(s(x0), x1)), c(z2, z3)) → c1(H(c(s(z2), c(s(x2), c(s(x0), x1))), z3))
H(c(s(s(0)), x0), c(x1, x2)) → c1(H(c(s(x1), c(s(s(0)), x0)), x2))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c2, c1

(7) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace H(c(s(z0), c(s(0), z1)), z2) → c2(H(z1, c(s(0), c(z0, z2)))) by

H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))
H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(x2), c(s(x0), x1)), c(z2, z3)) → c1(H(c(s(z2), c(s(x2), c(s(x0), x1))), z3))
H(c(s(s(0)), x0), c(x1, x2)) → c1(H(c(s(x1), c(s(s(0)), x0)), x2))
H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))

S tuples:

H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))
H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(x2), c(s(x0), x1)), c(z2, z3)) → c1(H(c(s(z2), c(s(x2), c(s(x0), x1))), z3))
H(c(s(s(0)), x0), c(x1, x2)) → c1(H(c(s(x1), c(s(s(0)), x0)), x2))
H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c1, c2

(9) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace H(c(s(x2), c(s(x0), x1)), c(z2, z3)) → c1(H(c(s(z2), c(s(x2), c(s(x0), x1))), z3)) by

H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))
H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(s(0)), x0), c(x1, x2)) → c1(H(c(s(x1), c(s(s(0)), x0)), x2))
H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))

S tuples:

H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))
H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(s(0)), x0), c(x1, x2)) → c1(H(c(s(x1), c(s(s(0)), x0)), x2))
H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c1, c2

(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace H(c(s(s(0)), x0), c(x1, x2)) → c1(H(c(s(x1), c(s(s(0)), x0)), x2)) by

H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))
H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))

S tuples:

H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2)))
H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c1, c2

(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace H(x1, c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), x1), c(x0, x2))) by

H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(0), c(s(y1), y2)), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), c(s(y1), y2))), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))
H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))

S tuples:

H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2)))
H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))
H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c1, c2

(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace H(c(s(z0), z1), c(s(0), c(x0, x2))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(x0, x2))) by

H(c(s(z0), z1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, y3))))
H(c(s(0), z1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), z1)), c(s(0), c(y2, y3))))
H(c(s(0), z1), c(s(0), c(z2, z3))) → c1(H(c(s(s(0)), c(s(0), z1)), c(z2, z3)))
H(c(s(0), c(s(y1), y2)), c(s(0), c(z2, z3))) → c1(H(c(s(s(0)), c(s(0), c(s(y1), y2))), c(z2, z3)))
H(c(s(z0), z1), c(s(0), c(z2, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(s(0), c(y4, y5)))))
H(c(s(z0), z1), c(s(0), c(z2, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y4, y5))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), z1), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, y2)))))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))
H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), z1), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, y2)))))

S tuples:

H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))
H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), z1), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, y2)))))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c2, c1

(17) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace H(c(s(x3), c(s(0), c(s(x1), x2))), x4) → c2(H(c(s(x1), x2), c(s(0), c(x3, x4)))) by

H(c(s(z0), c(s(0), c(s(z1), c(s(0), y1)))), z3) → c2(H(c(s(z1), c(s(0), y1)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), c(s(0), y0)))), z3) → c2(H(c(s(s(0)), c(s(0), y0)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), c(s(y1), y2))))), z3) → c2(H(c(s(z1), c(s(0), c(s(y1), y2))), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(y4, y5)) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(y1), y2)))), z3) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(y3, y4)) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(0), c(s(y0), y1)))), z3) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(y2, y3)) → c2(H(c(s(s(0)), z2), c(s(0), c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), z3) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(y3, y4)) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(0), z2))), c(y1, y2)) → c2(H(c(s(0), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(0), z2))), z3) → c2(H(c(s(0), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y3, y4)) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(y3, y4))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y1, y2))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(s(0), c(y4, y5))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(y4, y5)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, y3))))))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))
H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), z1), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), y1)))), z3) → c2(H(c(s(z1), c(s(0), y1)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), c(s(0), y0)))), z3) → c2(H(c(s(s(0)), c(s(0), y0)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), c(s(y1), y2))))), z3) → c2(H(c(s(z1), c(s(0), c(s(y1), y2))), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(y4, y5)) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(y1), y2)))), z3) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(y3, y4)) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(0), c(s(y0), y1)))), z3) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(y2, y3)) → c2(H(c(s(s(0)), z2), c(s(0), c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), z3) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(y3, y4)) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(0), z2))), c(y1, y2)) → c2(H(c(s(0), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(0), z2))), z3) → c2(H(c(s(0), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y3, y4)) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(y3, y4))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y1, y2))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(s(0), c(y4, y5))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(y4, y5)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, y3))))))

S tuples:

H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))
H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), z1), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), y1)))), z3) → c2(H(c(s(z1), c(s(0), y1)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), c(s(0), y0)))), z3) → c2(H(c(s(s(0)), c(s(0), y0)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), c(s(y1), y2))))), z3) → c2(H(c(s(z1), c(s(0), c(s(y1), y2))), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(y4, y5)) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(y1), y2)))), z3) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(y3, y4)) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(0), c(s(y0), y1)))), z3) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(y2, y3)) → c2(H(c(s(s(0)), z2), c(s(0), c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), z3) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(y3, y4)) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(0), z2))), c(y1, y2)) → c2(H(c(s(0), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(0), z2))), z3) → c2(H(c(s(0), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y3, y4)) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(y3, y4))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y1, y2))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(s(0), c(y4, y5))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(y4, y5)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, y3))))))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c2, c1

(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace H(c(s(z0), c(s(z1), z2)), c(z3, c(y3, y4))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(y3, y4))) by

H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(z0), c(s(z1), z2)), c(z3, c(z4, c(s(0), c(y4, y5))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(z4, c(y4, y5)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(z4, c(y4, y5))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y3, y4)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y3, y4))))
H(c(s(z0), c(s(z1), z2)), c(0, c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(z0), c(s(z1), z2)), c(0, c(z4, z5))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(z4, z5)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(0, c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(s(0), c(y2, y3)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5)))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, c(y4, y5))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y2, y3))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(y2, y3)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(0), c(s(z1), c(s(0), y2))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(0), y2)))), c(z4, z5)))
H(c(s(0), c(s(s(0)), c(s(0), y1))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), c(s(0), y1)))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(0), c(s(y2), y3)))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(0), c(s(y2), y3))))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(y1), y2))), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(y2), y3))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(y2), y3)))), c(z4, z5)))
H(c(s(0), c(s(0), c(s(y0), y1))), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(z4, z5)))
H(c(s(0), c(s(0), c(s(y1), y2))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(0), c(s(y1), y2)))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), z2))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(0), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(0), z2))), c(z4, z5)))
H(c(s(0), c(s(0), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(0), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, c(s(0), c(y4, y5))))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, c(y4, y5)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, c(y4, y5))))
H(c(s(0), c(s(z1), z2)), c(0, c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(0), c(s(z1), z2)), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(0, c(z4, z5))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, y4)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, y4))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, c(s(0), c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, c(s(0), c(y4, y5))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, c(y4, y5))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))
H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), z1), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), y1)))), z3) → c2(H(c(s(z1), c(s(0), y1)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), c(s(0), y0)))), z3) → c2(H(c(s(s(0)), c(s(0), y0)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), c(s(y1), y2))))), z3) → c2(H(c(s(z1), c(s(0), c(s(y1), y2))), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(y4, y5)) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(y1), y2)))), z3) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(y3, y4)) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(0), c(s(y0), y1)))), z3) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(y2, y3)) → c2(H(c(s(s(0)), z2), c(s(0), c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), z3) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(y3, y4)) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(0), z2))), c(y1, y2)) → c2(H(c(s(0), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(0), z2))), z3) → c2(H(c(s(0), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y3, y4)) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(y3, y4))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y1, y2))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(s(0), c(y4, y5))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(y4, y5)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(z4, c(s(0), c(y4, y5))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(z4, c(y4, y5)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(z4, c(y4, y5))))
H(c(s(z0), c(s(z1), z2)), c(0, c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(z0), c(s(z1), z2)), c(0, c(z4, z5))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(z4, z5)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(0, c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(s(0), c(y2, y3)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5)))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, c(y4, y5))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y2, y3))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(y2, y3)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(0), c(s(z1), c(s(0), y2))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(0), y2)))), c(z4, z5)))
H(c(s(0), c(s(s(0)), c(s(0), y1))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), c(s(0), y1)))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(0), c(s(y2), y3)))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(0), c(s(y2), y3))))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(y1), y2))), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(y2), y3))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(y2), y3)))), c(z4, z5)))
H(c(s(0), c(s(0), c(s(y0), y1))), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(z4, z5)))
H(c(s(0), c(s(0), c(s(y1), y2))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(0), c(s(y1), y2)))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), z2))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(0), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(0), z2))), c(z4, z5)))
H(c(s(0), c(s(0), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(0), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, c(s(0), c(y4, y5))))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, c(y4, y5)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, c(y4, y5))))
H(c(s(0), c(s(z1), z2)), c(0, c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(0), c(s(z1), z2)), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(0, c(z4, z5))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, y4)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, y4))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, c(s(0), c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, c(s(0), c(y4, y5))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, c(y4, y5))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))))

S tuples:

H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))
H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), z1), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), y1)))), z3) → c2(H(c(s(z1), c(s(0), y1)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), c(s(0), y0)))), z3) → c2(H(c(s(s(0)), c(s(0), y0)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), c(s(y1), y2))))), z3) → c2(H(c(s(z1), c(s(0), c(s(y1), y2))), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(y4, y5)) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(y1), y2)))), z3) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(y3, y4)) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(0), c(s(y0), y1)))), z3) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(y2, y3)) → c2(H(c(s(s(0)), z2), c(s(0), c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), z3) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(y3, y4)) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(0), z2))), c(y1, y2)) → c2(H(c(s(0), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(0), z2))), z3) → c2(H(c(s(0), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y3, y4)) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(y3, y4))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y1, y2))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(s(0), c(y4, y5))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(y4, y5)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(z4, c(s(0), c(y4, y5))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(z4, c(y4, y5)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(z4, c(y4, y5))))
H(c(s(z0), c(s(z1), z2)), c(0, c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(z0), c(s(z1), z2)), c(0, c(z4, z5))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(z4, z5)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(0, c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(s(0), c(y2, y3)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5)))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, c(y4, y5))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y2, y3))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(y2, y3)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(0), c(s(z1), c(s(0), y2))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(0), y2)))), c(z4, z5)))
H(c(s(0), c(s(s(0)), c(s(0), y1))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), c(s(0), y1)))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(0), c(s(y2), y3)))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(0), c(s(y2), y3))))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(y1), y2))), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(y2), y3))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(y2), y3)))), c(z4, z5)))
H(c(s(0), c(s(0), c(s(y0), y1))), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(z4, z5)))
H(c(s(0), c(s(0), c(s(y1), y2))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(0), c(s(y1), y2)))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), z2))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(0), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(0), z2))), c(z4, z5)))
H(c(s(0), c(s(0), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(0), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, c(s(0), c(y4, y5))))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, c(y4, y5)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, c(y4, y5))))
H(c(s(0), c(s(z1), z2)), c(0, c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(0), c(s(z1), z2)), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(0, c(z4, z5))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, y4)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, y4))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, c(s(0), c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, c(s(0), c(y4, y5))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, c(y4, y5))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c2, c1

(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace H(c(s(z0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(y1, y2))) by

H(c(s(0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z3, z4)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y3, y4))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(0, c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(0), c(s(z1), c(s(0), y2))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(0), y2)))), c(z3, z4)))
H(c(s(0), c(s(s(0)), c(s(0), y1))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), c(s(0), y1)))), c(z3, z4)))
H(c(s(0), c(s(z1), c(s(0), c(s(y2), y3)))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(0), c(s(y2), y3))))), c(z3, z4)))
H(c(s(0), c(s(z1), c(s(y1), y2))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(z3, z4)))
H(c(s(0), c(s(0), c(s(y0), y1))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(z3, z4)))
H(c(s(0), c(s(s(0)), z2)), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(z3, z4)))
H(c(s(0), c(s(s(0)), z2)), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(0), z2)), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(0), z2))), c(z3, z4)))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z3, c(s(0), c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z3, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z3, c(y4, y5))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z3, c(y3, c(s(0), c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z3, c(y3, c(s(0), c(y4, y5))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z3, c(y3, c(y4, y5))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z3, c(y3, c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, y5))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(s(0), c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(s(0), c(y5, y6))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(s(0), c(y5, y6)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(y5, y6)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(y5, y6))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(y5, c(s(0), c(y6, y7)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(y5, c(s(0), c(y6, y7))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(y5, c(y6, y7))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(y5, c(y6, y7)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(0, c(y4, c(s(0), c(y5, y6)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(0, c(y4, c(s(0), c(y5, y6))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(0, c(s(0), c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(0, c(s(0), c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(0, c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(0, c(y4, y5))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(s(0), c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(s(0), c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(s(0), c(y5, y6)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(s(0), c(y5, y6))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(y5, y6))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(y5, y6)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(s(0), c(y6, y7))))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(s(0), c(y6, y7)))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(y6, y7)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(y6, y7))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(0, c(y4, c(s(0), c(y5, y6))))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(0, c(y4, c(s(0), c(y5, y6)))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y4, y5)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(0, c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(0, c(y4, y5)))))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

h(z0, c(z1, z2)) → h(c(s(z1), z0), z2)
h(c(s(z0), c(s(0), z1)), z2) → h(z1, c(s(0), c(z0, z2)))

Tuples:

H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))
H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), z1), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), y1)))), z3) → c2(H(c(s(z1), c(s(0), y1)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), c(s(0), y0)))), z3) → c2(H(c(s(s(0)), c(s(0), y0)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), c(s(y1), y2))))), z3) → c2(H(c(s(z1), c(s(0), c(s(y1), y2))), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(y4, y5)) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(y1), y2)))), z3) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(y3, y4)) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(0), c(s(y0), y1)))), z3) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(y2, y3)) → c2(H(c(s(s(0)), z2), c(s(0), c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), z3) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(y3, y4)) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(0), z2))), c(y1, y2)) → c2(H(c(s(0), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(0), z2))), z3) → c2(H(c(s(0), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y3, y4)) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(y3, y4))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y1, y2))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(s(0), c(y4, y5))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(y4, y5)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(z4, c(s(0), c(y4, y5))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(z4, c(y4, y5)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(z4, c(y4, y5))))
H(c(s(z0), c(s(z1), z2)), c(0, c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(z0), c(s(z1), z2)), c(0, c(z4, z5))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(z4, z5)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(0, c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(s(0), c(y2, y3)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5)))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, c(y4, y5))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y2, y3))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(y2, y3)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(0), c(s(z1), c(s(0), y2))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(0), y2)))), c(z4, z5)))
H(c(s(0), c(s(s(0)), c(s(0), y1))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), c(s(0), y1)))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(0), c(s(y2), y3)))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(0), c(s(y2), y3))))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(y1), y2))), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(y2), y3))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(y2), y3)))), c(z4, z5)))
H(c(s(0), c(s(0), c(s(y0), y1))), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(z4, z5)))
H(c(s(0), c(s(0), c(s(y1), y2))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(0), c(s(y1), y2)))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), z2))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(0), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(0), z2))), c(z4, z5)))
H(c(s(0), c(s(0), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(0), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, c(s(0), c(y4, y5))))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, c(y4, y5)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, c(y4, y5))))
H(c(s(0), c(s(z1), z2)), c(0, c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(0), c(s(z1), z2)), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(0, c(z4, z5))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, y4)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, y4))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, c(s(0), c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, c(s(0), c(y4, y5))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, c(y4, y5))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(0, c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(0), c(s(z1), c(s(0), y2))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(0), y2)))), c(z3, z4)))
H(c(s(0), c(s(s(0)), c(s(0), y1))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), c(s(0), y1)))), c(z3, z4)))
H(c(s(0), c(s(z1), c(s(0), c(s(y2), y3)))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(0), c(s(y2), y3))))), c(z3, z4)))
H(c(s(0), c(s(s(0)), z2)), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(s(0), c(y2, y3))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, y5))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(s(0), c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(s(0), c(y5, y6))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(s(0), c(y5, y6)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(y5, y6)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(y5, y6))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(y5, c(s(0), c(y6, y7)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(y5, c(s(0), c(y6, y7))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(y5, c(y6, y7))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(y5, c(y6, y7)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(0, c(y4, c(s(0), c(y5, y6)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(0, c(y4, c(s(0), c(y5, y6))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(0, c(s(0), c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(0, c(s(0), c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(0, c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(0, c(y4, y5))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(s(0), c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(s(0), c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(s(0), c(y5, y6)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(s(0), c(y5, y6))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(y5, y6))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(y5, y6)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(s(0), c(y6, y7))))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(s(0), c(y6, y7)))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(y6, y7)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(y6, y7))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(0, c(y4, c(s(0), c(y5, y6))))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(0, c(y4, c(s(0), c(y5, y6)))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y4, y5)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(0, c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(0, c(y4, y5)))))))

S tuples:

H(c(s(z0), c(s(0), z1)), c(s(0), c(x0, x2))) → c2(H(z1, c(s(0), c(z0, c(s(0), c(x0, x2))))))
H(c(s(s(0)), c(s(0), z1)), c(x1, x2)) → c2(H(z1, c(s(0), c(s(0), c(x1, x2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, y2)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(0), c(s(z1), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)))
H(c(s(0), c(s(z1), z2)), c(z3, z4)) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), z4))
H(c(s(s(0)), z0), c(z1, c(s(0), c(y1, y2)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(s(0), c(y1, y2))))
H(c(s(s(0)), z0), c(s(0), c(y1, y2))) → c1(H(c(s(s(0)), c(s(s(0)), z0)), c(y1, y2)))
H(c(s(s(0)), z0), c(z1, c(y3, c(s(0), c(y4, y5))))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(s(0), c(y4, y5)))))
H(c(s(s(0)), z0), c(z1, c(y3, c(y4, y5)))) → c1(H(c(s(z1), c(s(s(0)), z0)), c(y3, c(y4, y5))))
H(c(s(s(0)), z0), c(0, c(y2, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, c(s(0), c(y3, y4)))))
H(c(s(s(0)), z0), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(s(0)), z0)), c(s(0), c(y2, y3))))
H(c(s(s(0)), z0), c(0, c(y2, y3))) → c1(H(c(s(0), c(s(s(0)), z0)), c(y2, y3)))
H(z0, c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(s(0), c(y1, y2))))
H(c(s(0), y1), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), y1)), c(s(0), c(y2, y3))))
H(c(s(0), y0), c(s(0), c(z1, z2))) → c1(H(c(s(s(0)), c(s(0), y0)), c(z1, z2)))
H(c(s(y1), y2), c(s(0), c(z1, c(s(0), c(y4, y5))))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(s(0), c(y4, y5)))))
H(c(s(y1), y2), c(s(0), c(z1, c(y4, y5)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(z1, c(y4, y5))))
H(c(s(y1), y2), c(s(0), c(s(0), c(y3, y4)))) → c1(H(c(s(s(0)), c(s(y1), y2)), c(s(0), c(y3, y4))))
H(z0, c(s(0), c(z1, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), z0), c(z1, c(s(0), c(y2, y3)))))
H(z0, c(s(0), c(z1, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(s(0), c(y3, y4))))))
H(z0, c(s(0), c(z1, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), z0), c(z1, c(y2, c(y3, y4)))))
H(z0, c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), z0), c(0, c(y1, c(s(0), c(y2, y3))))))
H(z0, c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), z0), c(0, c(s(0), c(y1, y2)))))
H(z0, c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), z0), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(z2, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(z2, c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), z1), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(0, c(y1, y2))))
H(c(s(z0), z1), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), z1), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), z1)), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), y1)))), z3) → c2(H(c(s(z1), c(s(0), y1)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), c(s(0), y0)))), z3) → c2(H(c(s(s(0)), c(s(0), y0)), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), c(s(0), c(s(y1), y2))))), z3) → c2(H(c(s(z1), c(s(0), c(s(y1), y2))), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(y4, y5)) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(0), c(s(z1), c(s(y1), y2)))), z3) → c2(H(c(s(z1), c(s(y1), y2)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(y3, y4)) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(0), c(s(y0), y1)))), z3) → c2(H(c(s(0), c(s(y0), y1)), c(s(0), c(z0, z3))))
H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(y2, y3)) → c2(H(c(s(s(0)), z2), c(s(0), c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), z3) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(s(0)), z2))), c(y3, y4)) → c2(H(c(s(s(0)), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(0), z2))), c(y1, y2)) → c2(H(c(s(0), z2), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(0), c(s(0), z2))), z3) → c2(H(c(s(0), z2), c(s(0), c(z0, z3))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(s(0), c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y3, y4)) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y3, y4)))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(z0, c(y2, c(y3, y4))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y1, y2))) → c2(H(c(s(z1), z2), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(0), c(s(0), c(s(z1), z2))), c(y1, y2)) → c2(H(c(s(z1), z2), c(s(0), c(0, c(y1, y2)))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(s(0), c(y3, y4)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, y4))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(s(0), c(y4, y5))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(y2, c(y3, c(y4, y5)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))) → c2(H(c(s(z1), z2), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(z4, c(s(0), c(y4, y5))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y4, y5)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(z4, c(y4, y5)))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(z4, c(y4, y5))))
H(c(s(z0), c(s(z1), z2)), c(0, c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(z0), c(s(z1), z2)), c(0, c(z4, z5))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(z4, z5)))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(s(0), c(y2, y3)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z4, c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z4, c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(y1, y2)))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(y1, y2))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(0, c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(0), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(s(0), c(y2, y3)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, y4)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5)))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(y2, c(y3, c(y4, y5))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y2, y3))))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(z3, c(s(0), c(s(0), c(0, c(y2, y3)))))) → c1(H(c(s(z3), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(0), c(s(z1), c(s(0), y2))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(0), y2)))), c(z4, z5)))
H(c(s(0), c(s(s(0)), c(s(0), y1))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), c(s(0), y1)))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(0), c(s(y2), y3)))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(0), c(s(y2), y3))))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(y1), y2))), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(y1), y2)))), c(z4, z5)))
H(c(s(0), c(s(z1), c(s(y2), y3))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), c(s(y2), y3)))), c(z4, z5)))
H(c(s(0), c(s(0), c(s(y0), y1))), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(0), c(s(y0), y1)))), c(z4, z5)))
H(c(s(0), c(s(0), c(s(y1), y2))), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(0), c(s(y1), y2)))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), z2))), c(z4, z5)))
H(c(s(0), c(s(s(0)), z2)), c(z3, c(s(0), c(y2, y3)))) → c1(H(c(s(z3), c(s(0), c(s(s(0)), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(0), z2)), c(s(0), c(z4, z5))) → c1(H(c(s(s(0)), c(s(0), c(s(0), z2))), c(z4, z5)))
H(c(s(0), c(s(0), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(0), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, z5))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, c(s(0), c(y4, y5))))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(z3, c(z4, c(y4, y5)))) → c1(H(c(s(z3), c(s(0), c(s(z1), z2))), c(z4, c(y4, y5))))
H(c(s(0), c(s(z1), z2)), c(0, c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(0), c(s(z1), z2)), c(0, c(s(0), c(y2, y3)))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(0, c(z4, z5))) → c1(H(c(s(0), c(s(0), c(s(z1), z2))), c(z4, z5)))
H(c(s(0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(s(0), c(y2, y3))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(s(0), c(y3, y4))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(s(0), c(y3, y4)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, y4)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, y4))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, c(s(0), c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, c(s(0), c(y4, y5))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(z4, c(y3, c(y4, y5))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(z4, c(y3, c(y4, y5)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, c(s(0), c(y3, y4))))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(y2, y3))))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(s(0), c(y2, y3)))))
H(c(s(0), c(s(z1), z2)), c(s(0), c(0, c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), z2))), c(0, c(y2, y3))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y2, c(y3, y4))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y2, c(y3, y4)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(y1, c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(y1, c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(0, c(y1, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(0, c(s(0), c(y1, y2)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(s(0), c(y1, y2))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(0, c(y1, y2))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(0, c(y1, y2)))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(s(0), c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(s(0), c(y2, y3))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(s(0), c(y3, y4)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(y2, c(y3, c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, c(s(0), c(y3, y4))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(s(0), c(y2, y3)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(s(0), c(s(0), c(0, c(y2, y3)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(s(0), c(s(0), c(0, c(y2, y3))))))
H(c(s(0), c(s(z1), c(s(0), y2))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(0), y2)))), c(z3, z4)))
H(c(s(0), c(s(s(0)), c(s(0), y1))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), c(s(0), y1)))), c(z3, z4)))
H(c(s(0), c(s(z1), c(s(0), c(s(y2), y3)))), c(s(0), c(z3, z4))) → c1(H(c(s(s(0)), c(s(0), c(s(z1), c(s(0), c(s(y2), y3))))), c(z3, z4)))
H(c(s(0), c(s(s(0)), z2)), c(s(0), c(s(0), c(y2, y3)))) → c1(H(c(s(s(0)), c(s(0), c(s(s(0)), z2))), c(s(0), c(y2, y3))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, y5))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(0, c(s(0), c(s(0), c(y3, y4)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(0, c(s(0), c(s(0), c(y3, y4))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(s(0), c(y5, y6))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(s(0), c(y5, y6)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(y5, y6)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(y5, y6))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(y5, c(s(0), c(y6, y7)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(y5, c(s(0), c(y6, y7))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(y4, c(y5, c(y6, y7))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(y4, c(y5, c(y6, y7)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(0, c(y4, c(s(0), c(y5, y6)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(0, c(y4, c(s(0), c(y5, y6))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(0, c(s(0), c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(0, c(s(0), c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(0, c(y4, y5)))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(0, c(y4, y5))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(s(0), c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(s(0), c(y4, y5)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(s(0), c(y5, y6)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(s(0), c(y5, y6))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(y5, y6))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(y5, y6)))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(s(0), c(y6, y7))))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(s(0), c(y6, y7)))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(y6, y7)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(y4, c(y5, c(y6, y7))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(0, c(y4, c(s(0), c(y5, y6))))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(0, c(y4, c(s(0), c(y5, y6)))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y4, y5)))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(0, c(s(0), c(y4, y5))))))))
H(c(s(z0), c(s(z1), z2)), c(s(0), c(z3, c(s(0), c(s(0), c(0, c(y4, y5))))))) → c1(H(c(s(s(0)), c(s(z0), c(s(z1), z2))), c(z3, c(s(0), c(s(0), c(0, c(y4, y5)))))))

K tuples:none
Defined Rule Symbols:

h

Defined Pair Symbols:

H

Compound Symbols:

c2, c1

(23) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
c0(0, 0) → 0
s0(0) → 0
00() → 0
h0(0, 0) → 1
s1(0) → 3
c1(3, 0) → 2
h1(2, 0) → 1
01() → 6
s1(6) → 5
c1(0, 0) → 7
c1(5, 7) → 4
h1(0, 4) → 1
c1(3, 2) → 2
s2(5) → 9
c2(9, 0) → 8
h2(8, 7) → 1
c1(0, 4) → 7
h1(2, 4) → 1
s2(0) → 9
c2(9, 8) → 8
h2(8, 0) → 1
h2(8, 4) → 1
c1(5, 7) → 7
c2(9, 2) → 8
c1(3, 8) → 2
c1(0, 7) → 7
c1(5, 0) → 7
c1(5, 4) → 7
h1(8, 4) → 1

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(20) Obligation:

(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(22) Obligation:

(23) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

(24) BOUNDS(O(1), O(n^1))